Home » Fiche   membre

Nicolas TABAREAU

CHERCHEUR

HDR

: Nicolas.Tabareauatls2n.fr

Adresse :

IMT Atlantique Bretagne-Pays de la Loire Ecole Mines-Telecom ( IMT ATLANTIQUE )
La Chantrerie
4, rue Alfred Kastler
B.P. 20722
44307 NANTES Cedex 3


Publications référencées sur HAL

Revues internationales avec comité de lecture (ART_INT)

    • [1] Y. Forster, M. Sozeau, N. Tabareau. Verified Extraction from Coq to OCaml. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2024, vol. 8, num. PLDI.
      https://inria.hal.science/hal-04329663v1
    • [2] M. Malewski, K. Maillard, N. Tabareau, Ã. Tanter. Gradual Indexed Inductive Types. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2024, vol. 8, num. ICFP.
      https://inria.hal.science/hal-04681546v1
    • [3] L. Pujet, N. Tabareau. Impredicative Observational Equality. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2023, vol. 7, num. POPL.
      https://hal.science/hal-03857705v2
    • [4] M. Lennon-Bertrand, K. Maillard, N. Tabareau, Ã. Tanter. Gradualizing the Calculus of Inductive Constructions. In ACM Transactions on Programming Languages and Systems (TOPLAS) ; éd. ACM, 2022.
      https://hal.science/hal-02896776v5
    • [5] K. Maillard, M. Lennon-Bertrand, N. Tabareau, Ã. Tanter. A Reasonably Gradual Type Theory. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2022.
      https://inria.hal.science/hal-03596652v2
    • [6] L. Pujet, N. Tabareau. Observational Equality: Now For Good. In POPL 2022: Symposium on Principles of Programming Languages, janvier 2022, Philadelphia, états-Unis.In Proceedings of the ACM on Programming Languages ; éd. ACM, 2022, vol. 6, num. POPL.
      https://inria.hal.science/hal-03367052v4
    • [7] J. Cockx, N. Tabareau, T. Winterhalter. The Taming of the Rew: A Type Theory with Computational Assumptions. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2021.
      https://hal.science/hal-02901011v2
    • [8] N. Tabareau, Ã. Tanter, M. Sozeau. The Marriage of Univalence and Parametricity. In Journal of the ACM (JACM) ; éd. Association for Computing Machinery, 2021, vol. 68, num. 1.
      https://inria.hal.science/hal-03120580v1
    • [9] M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, T. Winterhalter. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2020.
      https://hal.science/hal-02380196v2
    • [11] M. Sozeau, A. Anand, S. Boulier, C. Cohen, Y. Forster, F. Kunze, G. Malecha, N. Tabareau, T. Winterhalter. The MetaCoq Project. In Journal of Automated Reasoning ; éd. Springer Verlag, 2020.
      https://inria.hal.science/hal-02167423v1
    • [12] S. Boulier, N. Tabareau. Model structure on the universe of all types in interval type theory. In Mathematical Structures in Computer Science ; éd. Cambridge University Press (CUP), 2020.
      https://inria.hal.science/hal-02966633v1
    • [13] G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau. Definitional Proof-Irrelevance without K. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2019.
      https://inria.hal.science/hal-01859964v2
    • [15] P. Pédrot, N. Tabareau, H. Fehrmann, Ã. Tanter. A Reasonably Exceptional Type Theory. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2019, vol. 3.
      https://inria.hal.science/hal-02189128v1
    • [16] P. Dagand, N. Tabareau, Ã. Tanter. Foundations of Dependent Interoperability. In Journal of Functional Programming ; éd. Cambridge University Press (CUP), 2018, vol. 28.
      https://inria.hal.science/hal-01629909v2
    • [17] P. Melliès, N. Tabareau, C. Tasson. An explicit formula for the free exponential modality of linear logic. In Mathematical Structures in Computer Science ; éd. Cambridge University Press (CUP), 2018, vol. 28, num. 7.
      https://inria.hal.science/hal-01992148v1
    • [19] P. Lefanu Lumsdaine, N. Tabareau. Preface: Special Issue on Homotopy Type Theory and Univalent Foundations. In Journal of Automated Reasoning ; éd. Springer Verlag, 2018.
      https://inria.hal.science/hal-01929871v1
    • [20] K. Quirin, N. Tabareau. Lawvere-Tierney sheafification in Homotopy Type Theory. In Journal of Formalized Reasoning ; éd. ASDD-AlmaDL, 2016, vol. 9, num. 2.
      https://inria.hal.science/hal-01451710v1
    • [21] I. Figueroa, N. Tabareau, Ã. Tanter. Effect capabilities for Haskell: Taming effect interference in monadic programming. In Science of Computer Programming ; éd. Elsevier, 2016, vol. 119.
      https://inria.hal.science/hal-01400002v1
    • [22] I. Figueroa, N. Tabareau, Ã. Tanter. Effective Aspects: A Typed Monadic Embedding of Pointcuts and Advice. In LNCS Transactions on Aspect-Oriented Software Development ; éd. Springer, 2014.
      https://inria.hal.science/hal-00872782v1
    • [23] Ã. Tanter, I. Figueroa, N. Tabareau. Execution Levels for Aspect-Oriented Programming: Design, Semantics, Implementations and Applications. In Science of Computer Programming ; éd. Elsevier, 2014, vol. 80, num. 1.
      https://inria.hal.science/hal-00872786v1
    • [25] P. Melliès, N. Tabareau. Resource modalities in tensor logic. In Annals of Pure and Applied Logic ; éd. Elsevier Masson, 2010, vol. 161, num. 5.
      https://hal.science/hal-00339154v2
    • [26] Q. Pham, N. Tabareau, J. Slotine. A contraction theory approach to stochastic incremental stability. In IEEE Transactions on Automatic Control ; éd. Institute of Electrical and Electronics Engineers, 2009, vol. 54, num. 4.
      https://inria.hal.science/inria-00466264v1
    • [27] N. Tabareau, D. Bennequin, A. Berthoz, J. Slotine, B. Girard. Geometry of the superior colliculus mapping and efficient oculomotor computation. In Biological Cybernetics (Modeling) ; éd. Springer Verlag, 2007, vol. 97, num. 4.
      https://hal.science/hal-00178144v1

Conférences internationales avec comité de lecture et actes (COMM_INT)

    • [28] L. Pujet, N. Tabareau. Observational Equality Meets CIC. In ESOP 2024 - 33rd European Symposium on Programming, avril 2024, Luxembourg, Luxembourg.
      https://hal.science/hal-04535982v1
    • [29] Y. Leray, G. Gilbert, N. Tabareau, T. Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In International Conference on Interactive Theorem Proving (ITP 2024), septembre 2024, Tbilisi, Géorgie.
      https://inria.hal.science/hal-04511667v2
    • [30] G. Gilbert, P. Pédrot, M. Sozeau, N. Tabareau. From Lost to the River: Embracing Sort Proliferation. In TYPES 2023 - 29th International Conference on Types for Proofs and Programs, juin 2023, Valencia, Espagne.
      https://inria.hal.science/hal-04378939v1
    • [31] G. Gilbert, Y. Leray, N. Tabareau, T. Winterhalter. The Rewster: The Coq Proof Assistant with Rewrite Rules. In TYPES 2023 - 29th International Conference on Types for Proofs and Programs, juin 2023, Valencia, Espagne.
      https://inria.hal.science/hal-04403667v1
    • [32] T. Winterhalter, M. Sozeau, N. Tabareau. Eliminating Reflection from Type Theory. In CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, janvier 2019, Lisbonne, Portugal.
      https://hal.science/hal-01849166v3
    • [33] T. Altenkirch, S. Boulier, A. Kaposi, N. Tabareau. Setoid type theory - a syntactic translation. In MPC 2019 - 13th International Conference on Mathematics of Program Construction, octobre 2019, Porto, Portugal.
      https://inria.hal.science/hal-02281225v1
    • [34] A. Anand, S. Boulier, N. Tabareau, M. Sozeau. Typed Template Coq -- Certified Meta-Programming in Coq. In CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages, janvier 2018, Los Angeles, CA, états-Unis.
      https://inria.hal.science/hal-01671948v1
    • [35] P. Pédrot, N. Tabareau. Failure is Not an Option An Exceptional Type Theory. In ESOP 2018 - 27th European Symposium on Programming, avril 2018, Thessaloniki, Grèce.
      https://inria.hal.science/hal-01840643v1
    • [36] A. Anand, S. Boulier, C. Cohen, M. Sozeau, N. Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. In ITP 2018 - 9th Conference on Interactive Theorem Proving, juillet 2018, Oxford, Royaume-Uni.
      https://hal.science/hal-01809681v1
    • [37] S. Boulier, P. Pédrot, N. Tabareau. The next 700 syntactical models of type theory. In Certified Programs and Proofs (CPP 2017), janvier 2017, Paris, France.
      https://inria.hal.science/hal-01445835v1
    • [38] P. Pédrot, N. Tabareau. An Effectful Way to Eliminate Addiction to Dependence. In Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, juin 2017, Reykjavik, Islande.
      https://inria.hal.science/hal-01441829v1
    • [39] G. Jaber, G. Lewertowski, P. Pédrot, M. Sozeau, N. Tabareau. The Definitional Side of the Forcing. In Logics in Computer Science, mai 2016, New York, états-Unis.
      https://hal.science/hal-01319066v1
    • [40] P. Dagand, N. Tabareau, Ã. Tanter. Partial Type Equivalences for Verified Dependent Interoperability. In ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming, septembre 2016, Nara, Japon.
      https://inria.hal.science/hal-01328012v1
    • [41] A. Hirschowitz, T. Hirschowitz, N. Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. In Typed Lambda Calculi and Applications, 2015, Varsovie, Pologne.
      https://hal.science/hal-01178301v1
    • [42] Ã. Tanter, N. Tabareau. Gradual Certified Programming in Coq. In 11th ACM Dynamic Languages Symposium (DLS 2015), octobre 2015, Pittsburgh, états-Unis.
      https://inria.hal.science/hal-01238774v1
    • [43] I. Figueroa, T. Schrijvers, N. Tabareau, Ã. Tanter. Compositional Reasoning About Aspect Interference. In 13th International Conference on Modularity (Modularity'14), avril 2014, Lugano, Suisse.
      https://inria.hal.science/hal-00919935v1
    • [46] R. Douence, N. Tabareau. Lazier Imperative Programming. In Principles and Practice of Declarative Programming (PPDP), septembre 2014, Canterbury, Royaume-Uni.
      https://inria.hal.science/hal-01016565v1
    • [47] I. Figueroa, N. Tabareau, Ã. Tanter. Effect Capabilities For Haskell. In Brazilian Symposium on Programming Languages (SBLP), septembre 2014, Maceio, Brésil.
      https://inria.hal.science/hal-01038053v1
    • [48] N. Tabareau, I. Figueroa, Ã. Tanter. A Typed Monadic Embedding of Aspects. In 12th annual international conference on Aspect-Oriented Software Development (Modularity-AOSD'13), mars 2013, Fukuoka, Japon.
      https://inria.hal.science/hal-00763695v1
    • [49] I. Figueroa, N. Tabareau, Ã. Tanter. Taming aspects with monads and membranes. In FOAL'13: Foundations of aspect-oriented languages, mars 2013, Fukuoka, Japon.
      https://inria.hal.science/hal-00808983v1
    • [53] G. Jaber, N. Tabareau, M. Sozeau. Extending Type Theory with Forcing. In LICS 2012 : Logic In Computer Science, juin 2012, Dubrovnik, Croatie.
      https://hal.science/hal-00685150v1
    • [54] N. Tabareau. Aspect oriented programming: a language for 2-categories. In Proceedings of the 10th international workshop on Foundations of aspect-oriented languages, mars 2011, Porto de Galinhas, Brésil.
      https://inria.hal.science/inria-00583429v1
    • [55] N. Tabareau. A theory of distributed aspects. In 9th International Conference on Aspect-Oriented Software Development (AOSD '10), mars 2010, Rennes, Saint-Malo, France.In ACM (éds.), . , 2010.
      https://inria.hal.science/inria-00423996v4
    • [56] N. Benton, N. Tabareau. Compiling Functional Types to Relational Specifications for Low Level Imperative Code. In Types in Language Design and Implementation, janvier 2009, Savannah, états-Unis.
      https://hal.science/hal-00341404v1
    • [57] P. Melliès, N. Tabareau, C. Tasson. An explicit formula for the free exponential modality of linear logic. In 36th International Colloquium on Automata, Languages and Programming, juillet 2009, Rhodes, Grèce.
      https://hal.science/hal-00391714v2
    • [58] P. Melliès, N. Tabareau. An algebraic account of references in game semantics. In Mathematical Foundations of Programming Semantics, avril 2009, Oxford, Royaume-Uni.In Electronic Notes in Theoretical Computer Science (éds.), Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009). , 2009.
      https://hal.science/hal-00374933v2
    • [59] P. Melliès, N. Tabareau, C. Tasson. An explicit formula for the free exponential modality of linear logic. In ICALP 2009 : 36th International Colloquium on Automata, Languages, and Programming, juillet 2009, Rhodes, Grèce.In Mathematical Structures in Computer Science ; éd. Cambridge University Press (CUP), 2009.
      https://hal.science/hal-02436316v1
    • [60] L. Manfredi, E. Maini, P. Dario, C. Laschi, B. Girard, N. Tabareau, A. Berthoz. Implementation of a neurophysiological model of saccadic eye movements on an anthropomorphic robotic head. In 6th IEEE-RAS International Conference on Humanoid Robots, décembre 2006, Gênes, Italie.
      https://hal.science/hal-01525198v1
    • [61] B. Girard, N. Tabareau, J. Slotine, A. Berthoz. Contracting model of the basal ganglia. In Modeling Natural Action Selection, 2005, Edinburgh, Royaume-Uni.In Bryson, J., Prescott, T. and Seth, A. (éds.), . AISB Press, 2005.
      https://hal.science/hal-00016414v1
    • [62] D. d'Souza, N. Tabareau. On timed automata with input-determined guards. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, septembre 2004, , France.In yassine Lakhnech (éds.), Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. springer-verlag, 2004.
      https://hal.science/hal-00017462v1

Conférences nationales avec comité de lecture et actes (COMM_NAT)

    • [63] S. Boulier, P. Pédrot, N. Tabareau. Modèles de la théorie des types donnés par traduction de programme. In 28ièmes Journées Francophones des Langages Applicatifs, janvier 2017, Gourette, France.
      https://hal.science/hal-01503089v1
    • [64] N. Tabareau, Ã. Tanter, I. Figueroa. Anti-Unification with Type Classes. In Journées Francophones des Langages Applicatifs (JFLA), février 2013, Aussois, France.
      https://inria.hal.science/hal-00765862v1
    • [65] G. Jaber, N. Tabareau. The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code. In Workshop LOLA 2011, Syntax and Semantics of Low Level Languages, juin 2011, Toronto, Canada.
      https://hal.science/hal-00594386v1
    • [66] G. Jaber, N. Tabareau. Krivine realizability for compiler correctness. In Workshop LOLA 2010, Syntax and Semantics of Low Level Languages, juillet 2010, Edinburgh, Royaume-Uni.
      https://hal.science/hal-00475210v2
    • [67] B. Girard, N. Tabareau, A. Berthoz, J. Slotine. Selective amplification using a contracting model of the basal ganglia. In NeuroComp 2006, 2006, Pont A Mousson, France.In Alexandre, F., Boniface, Y., Bougrain, L., Girau, B. and Rougier, N. (éds.), . , 2006.
      https://hal.science/hal-00111145v1

Theses et HDR (THESE)

Autres publications (AUTRES)

Copyright : LS2N 2017 - Mentions Légales - 
 -